ds:x:Id fp Type, da:k:Knd fp Type, A, B:ecl-trans-tuple{i:l}(ds;da), f:(()()),
g:().
combine-ecl-tuples(A;B;f;g)  ecl-trans-tuple{i:l}(ds;da) 

latex

Definitions

t  T, x:A. B(x), State(ds), Valtype(da;k), false, Knd, (x  l), b, Prop, A, b, , AB, P  Q, False, , x. t(x), 2of(t), 1of(t), p  q, P & Q, P  Q, Unit, if b t else f fi, as @ bs, strong-subtype(A;B), EqDecider(T), a:A fp B(a), f(x)?z, , merge(as;bs), let a,b,c,d,e,f,g = u in v(a;b;c;d;e;f;g), combine-ecl-tuples(A;B;f;g), ecl-trans-tuple{i:l}(ds;da), Id, KindDeq, deq-member(eq;x;L)

Lemmas

ecl-trans-tuple wf, fpf wf, Id wf, merge wf, nat plus wf, nat wf, nat properties, strong-subtype-deq-subtype, strong-subtype-set3, strong-subtype-self, subtype rel self, l member subtype, append wf, ifthenelse wf, eqtt to assert, eqff to assert, iff transitivity, assert of bnot, not functionality wrt iff, assert-deq-member, deq-member wf, band wf, pi1 wf, pi2 wf, le wf, bool wf, bnot wf, not wf, assert wf, l member wf, Knd wf, Kind-deq wf, bfalse wf, ma-valtype wf, decl-state wf